$\vdash$  $\forall$$b$:$\mathbb{B}$, $P$, $Q$:Top. if $x$:$\uparrow$$b$ then $P$ else $Q$ fi  $\sim$ if $b$ then $P$ else $Q$ fi